package tests;

import controler.DesktopApplication;
import java.io.File;
import java.io.FileInputStream;
import java.util.LinkedList;
import java.io.FileNotFoundException;
import java.io.InputStreamReader;
import java.io.UnsupportedEncodingException;
import model.Formula;

import model.Prover;
import model.Operator;

public class Tests {

    /**
     * test modelu aplikacji
     */
    public static void modelProver() {
        System.out.println("\nTests.modelProver() - start");

        LinkedList<Operator> operators;
        try {
            operators = Operator.loadOperators(new InputStreamReader(new FileInputStream("operators.txt"), "UTF8"));
        } catch (FileNotFoundException fnfe) {
            fnfe.printStackTrace();
            return;
        } catch (UnsupportedEncodingException uee) {
            uee.printStackTrace();
            return;
        }

        String formula;
        try {
            formula = DesktopApplication.loadFormula("formula.txt");

            Tests.modelProverParenthesesValidator(formula, operators);

            Tests.modelProverCombination(formula, operators);
            //Tests.modelProverCombination("", operators);
            // Tests.modelProverCombination(formula, new
            // LinkedList<Operator>());
            // Tests.modelProverCombination("", new LinkedList<Operator>()); 
        } catch (Exception e) {
            e.printStackTrace();
        }

        System.out.println("Tests.modelProver() - stop\n");
    }
    
    static void modelProverParenthesesValidator(String formula, LinkedList<Operator> operators)
            throws Exception {
        System.out.println("\nTests.modelProverParenthesesValidator() - start");

        System.out.println("walidacja forumuły: " + formula);
        boolean correct = Formula.validate(formula, operators);
        System.out.println("zwalidowana jako: " + correct);

        System.out.println("Tests.modelProverParenthesesValidator() - stop\n");
    }

    static private void modelProverCombination(String formula, LinkedList<Operator> operators)
            throws Exception {
        System.out.println("\nTests.modelProverCombination() - start");

        System.out.println("formula: " + formula);

        System.out.println("operatory (" + operators.size() + "):");
        for (Operator o : operators) {
            System.out.println(o);
        }

        Prover p;
        boolean prove, state;
        System.out.println("\ntest dla 4 opcji warunku stopu i negacji:\n");
        for (int negate = -2; negate < 3; negate++) {
            if (negate == 0) {
                negate++;
            }
            p = new Prover(formula, operators, negate);
            System.out.println("prover     " + negate);
            try {
                prove = p.prove();
            } catch (Exception e) {
                e.printStackTrace();
                continue;
            }
            System.out.println("prove()    " + prove);
            state = p.getState();
            System.out.println("getState() " + state);
            System.out.println("zgodnosc:  " + (prove == state) + "\n");
            
            System.out.println("\nprzed zapisem do pliku");
            p.saveTree("graph.xml");
            System.out.println("zapisano do graph.xml");
        }        
        
        System.out.println("Tests.modelProverCombination() - stop\n");
    }

    public static void main(String[] arg) {
        System.out.println("THE MUFFIN PROJECT - start");

        Tests.modelProver();

        System.out.println("THE MUFFIN PROJECT - stop");
    }
}
